Rpre(${\it loc}$; ${\it ds}$; $a$; $p$; $P$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr inr inr inr inr inr inr (inl $<$${\it loc}$, ${\it ds}$, $a$, $p$, $P$$>$ )